00100	GIVEAX(DEFORD,(∀ R)
00200		(ORDERING R ≡ RELATION R ∧ IRREF R ∧ TRANSITIVE R));
00300	
00400	GIVEAX(IRREF,(∀ R)(IRREF R ≡ (∀ X)(∀ Y)(XεDOMAIN R
00500	∧YεDOMAIN R ∧ ββ(X,R,Y) ∧ ββ(Y,R,X) ⊃ X=Y)));
00600	
00700	GIVEAX(TRANSITIVE,(∀ R)(TRANSITIVE R≡ (∀ X)(∀ Y)(∀ Z)(
00800	XεDOMAIN R ∧ YεDOMAIN R ∧ Z ε DOMAIN R ∧
00900	ββ(X,R,Y) ∧ ββ(Y,R,Z) ⊃ ββ(X,R,Z))));
01000	
01100	GIVEAX(ASCENDSEQ,(∀ R)(∀ S)(ASCENDSEQ(R,S)≡ ORDERING R ∧
01200	Sε(I0→DOMAIN R) ∧ MONOTONIC(S,LE,R)));
01300	
01400	GIVEAX(MONOTONIC,(∀ F)(∀ R1)(∀ R2)(MONOTONIC(F,R1,R2) ≡
01500	ORDERING R1 ∧ ORDERING R2 ∧ Fε(DOMAIN R1 → DOMAIN R2)
01600	∧ (∀ X)(∀ Y)(XεDOMAIN(R1)∧YεDOMAIN(R1)∧ββ(X,R1,Y)
01700	⊃ββ(β(F,X),R2,β(F,Y)))));
01800	
01900	GIVEAX(CONTINUOUS,(∀ F)(∀ R1)(∀ R2)(CONTINUOUS(F,R1,R2) ≡
02000	MONOTONIC(F,R1,R2) ∧ (∀ S1)(∀ S2)(ASCENDSEQ(R1,S1) ∧
02100	ASCENDSEQ(R2,S2) ∧ ((∀ N)(NεI0 ⊃ β(F,β(S1,N))=β(S2,N))
02200	⊃β(F,LUB S1)=LUB S2))));
     

00100	END;